package strain.solver;

import java.util.Arrays;
import java.util.LinkedList;
import java.util.List;
import java.util.Queue;
import java.util.Set;

import strain.domain.Domain;
import strain.domain.InconsistentDomainException;
import strain.domain.BoolDomain;
import strain.domain.IntDomain;
import strain.domain.EnumDomain;
import strain.domain.RealDomain;
import strain.expression.BoolExpression;
import strain.expression.EnumExpression;
import strain.expression.Expression;
import strain.expression.IntExpression;
import strain.expression.RealExpression;
import util.Stack;

public class Solver {
    
    private static class SearchNode{
        public final SolverState state;
        public final Expression<?,?> branchExpression;
        public final Queue<?> domainPartition;
        public SearchNode(final SolverState state, final Expression<?,?> branchExpression, final Queue<?> domainPartition){
            this.state = state;
            this.branchExpression = branchExpression;
            this.domainPartition = domainPartition;
        }
    }
    
    private final SolverState initialState;
    private final BranchChooser branchChooser;
    private final DomainPartitioner domainPartitioner;
    
    public Solver(){
        // no objective, constructs a solver for checking feasibility only...
        this.initialState = new SolverState();
        this.branchChooser = new SmallestBranchChooser();
        this.domainPartitioner = new DichotomizingDomainPartitioner();
    }
    
//    public Solver(final List<Objective> prioritizedObjectives){
//
//    }
//
//    public Solver(final Objective objective){
//        this(Arrays.asList(objective));
//    }
    
    public <T, D extends Domain<T>> void add(final Expression<T,D> expression){
        expression.addTo(this.initialState);
    }
    
    public <T, D extends Domain<T>> Expression<T,D> get(final Expression<T, D> expression){
        return this.initialState.get(expression);
    }
    
    public boolean solve(){
        SolverState state = this.initialState.copy();
        try {
            state.reduceDomains();
        } catch (InconsistentDomainException e) {
            return false;
        }
        if (state.isBound()){
            return true;
        }
        Stack<SearchNode> stack = new Stack<SearchNode>();
        
        Expression<?,?> branchExpression = this.branchChooser.chooseBranchExpression(state.getExpressions());
        
        Queue<?> domainPartition = this.domainPartitioner.partitionDomain(branchExpression);
        stack.push(new SearchNode(state, branchExpression, domainPartition));

        while(!stack.isEmpty()){
            SearchNode node = stack.pop();
            branchExpression = node.branchExpression;
            domainPartition = node.domainPartition;
            Object subset = domainPartition.poll();
            if (!domainPartition.isEmpty()){
                stack.push(new SearchNode(node.state, branchExpression, domainPartition));
            }
            SolverState newState = node.state.copy();
            try{
                newState.get(branchExpression).retain(subset);
                newState.reduceDomains();
                if (newState.isBound()){
                    for(Expression<?,?> expression: this.initialState.getExpressions()){
                        expression.bind(newState.get(expression).getBoundValue());
                    }
                } else {
                    Expression<?,?> newBranchExpression = this.branchChooser.chooseBranchExpression(newState.getExpressions());
                    Queue<?> newDomainPartition = this.domainPartitioner.partitionDomain(newBranchExpression);
                    stack.push(new SearchNode(newState, newBranchExpression, newDomainPartition));
                }
            } catch (InconsistentDomainException ide) {
                // backtrack... do nothing... log no good?
            }
        }
        return false;
    }
    
}
